Natural number game
Leanで自然数(Natural number)に関連することをステージ形式で解いて行くWebアプリ
Leanで証明を書くってのがどんなものかを把握するにはとても良いもの
証明で使ういろいろなタクティクの使い方がわかるのでやるとお得
Lean 3版
Natural number game
Lean 4版
Natural Number Game
rfl 反射律 A = A
rw rewriteタクティク
code:memo
rfl
rw h
rw two_eq_succ_one
// 右辺にタクティクを適用する
rw \l one_eq_succ_zero
答え:
natural_number_game/SOLUTIONS.md at master · ImperialCollegeLondon/natural_number_game
adyavanapalli/natural-number-game-solutions: Solutions to Imperial College London's Natural Number Game, a gamified formal mathematics course on the Peano axioms using an interactive + automated theorem prover developed by Microsoft Research called Lean.
自然数游戏（Natural Number Game）答案合集 - 哔哩哔哩
自分が解いたログは下記
Proj: Natural number gameを解く
確認用
Q. Natural Number Game
メモ
Natural Number Game = Lean による定理証明支援を学ぶ - Maxima で綴る数学の旅
【Natural Number Game】指数法則も定理証明支援系で証明！#2 【Lean 4】 - YouTube
https://www.youtube.com/watch?v=rY_Q4rbdxK4
#Lean #定理証明支援系